(set-option :produce-interpolants 1)
(set-option :certify-interpolants 1)
(set-logic QF_UF)
(declare-sort Real 0)
(declare-fun .uf-not () Bool)
(declare-fun ite (Bool Real Real ) Real)
(declare-fun - (Real ) Real)
(declare-fun * (Real Real ) Real)
(declare-fun / (Real Real ) Real)
(declare-fun + (Real Real ) Real)
(declare-fun - (Real Real ) Real)
(declare-fun < (Real Real ) Bool)
(declare-fun <= (Real Real ) Bool)
(declare-fun > (Real Real ) Bool)
(declare-fun >= (Real Real ) Bool)
(declare-fun |hifrog::fun_start!0#5| () Bool)
(declare-fun |hifrog::fun_end!0#5| () Bool)
(declare-fun |goto_symex::guard#3| () Bool)
(declare-fun |func::a!0#4| () Real)
(declare-fun |func::a!0#2| () Real)
(declare-fun |func::b!0#4| () Real)
(declare-fun |func::b!0#2| () Real)
(declare-const 1 () Real)
(declare-fun |func::$tmp::return_value!0#5| () Real)
(declare-const 2 () Real)
(declare-fun |func::1::m!0#16| () Real)
(declare-fun |hifrog::c::unsupported_op2varsignedbv!0#0| () Real)
(declare-fun uns_mod (Real Real ) Real)
(declare-fun |func::1::m!0#17| () Real)
(declare-fun |func::1::m!0#18| () Real)
(declare-fun |func::1::m!0#19| () Real)
(declare-fun |func::1::m!0#20| () Real)
(declare-fun |func::1::m!0#21| () Real)
(declare-fun |func::1::m!0#22| () Real)
(declare-fun |func::1::m!0#23| () Real)
(declare-fun |func::1::m!0#24| () Real)
(declare-fun |func::1::m!0#25| () Real)
(declare-fun |func::$tmp::return_value!0#7| () Real)
(declare-fun |func::$tmp::return_value!0#8| () Real)
(declare-fun .oite0 () Real)
(declare-fun |func::#return_value!0#2| () Real)
(declare-fun |hifrog::fun_start!0#4| () Bool)
(declare-fun |hifrog::fun_end!0#4| () Bool)
(declare-fun |goto_symex::guard#2| () Bool)
(declare-fun |func::a!0#3| () Real)
(declare-fun |func::a!0#1| () Real)
(declare-fun |func::b!0#3| () Real)
(declare-fun |func::b!0#1| () Real)
(declare-fun |func::$tmp::return_value!0#1| () Real)
(declare-fun |func::1::m!0#3| () Real)
(declare-fun |hifrog::c::unsupported_op2varsignedbv!0#1| () Real)
(declare-fun |func::1::m!0#4| () Real)
(declare-fun |func::1::m!0#5| () Real)
(declare-fun |func::1::m!0#6| () Real)
(declare-fun |func::1::m!0#7| () Real)
(declare-fun |func::1::m!0#8| () Real)
(declare-fun |func::1::m!0#9| () Real)
(declare-fun |func::1::m!0#10| () Real)
(declare-fun |func::1::m!0#11| () Real)
(declare-fun |func::1::m!0#12| () Real)
(declare-fun |func::$tmp::return_value!0#3| () Real)
(declare-fun |func::$tmp::return_value!0#4| () Real)
(declare-fun .oite1 () Real)
(declare-fun |func::#return_value!0#1| () Real)
(declare-fun |hifrog::fun_start!0#3| () Bool)
(declare-fun |hifrog::fun_end!0#3| () Bool)
(declare-fun |hifrog::?err!0#2| () Bool)
(declare-fun |main::1::a!0#2| () Real)
(declare-fun |symex::nondet#0| () Real)
(declare-fun |main::1::b!0#2| () Real)
(declare-fun |symex::nondet#1| () Real)
(declare-fun |main::1::c!0#2| () Real)
(declare-fun |main::1::d!0#2| () Real)
(declare-fun |main::1::p!0#2| () Real)
(declare-fun |main::1::q!0#2| () Real)
(declare-const -999 () Real)
(declare-const 1000 () Real)
(declare-fun |hifrog::fun_start!0#2| () Bool)
(declare-fun |hifrog::fun_end!0#2| () Bool)
(declare-fun |hifrog::fun_start!0#1| () Bool)
(declare-fun |hifrog::fun_end!0#1| () Bool)
(declare-fun |hifrog::?err!0#1| () Bool)
(declare-fun |return'!0#1| () Real)
(declare-fun |symex::io::0| () Real)
; XXX oite symbol: (0 out of 1) .oite0
(assert (!(and (or (not |goto_symex::guard#3|) (= |func::$tmp::return_value!0#5| .oite0)) (or |goto_symex::guard#3| (= |func::$tmp::return_value!0#7| .oite0)))
:named a))
; XXX oite symbol: (1 out of 1) .oite1
(assert (!(and (or (not |goto_symex::guard#2|) (= |func::$tmp::return_value!0#1| .oite1)) (or |goto_symex::guard#2| (= |func::$tmp::return_value!0#3| .oite1)))
:named b))
; XXX Partition: 4
(assert (! 
(and (= |func::a!0#4| |func::a!0#2|) (= |func::b!0#4| |func::b!0#2|) (= |goto_symex::guard#3| (>= (+ |func::a!0#4| |func::b!0#4|) 1)) (= |func::$tmp::return_value!0#5| (/ (+ |func::a!0#4| |func::b!0#4|) 2)) (= |hifrog::c::unsupported_op2varsignedbv!0#0| (uns_mod |func::a!0#4| |func::b!0#4|)) (= |func::1::m!0#16| (+ 1 |hifrog::c::unsupported_op2varsignedbv!0#0|)) (= |func::1::m!0#17| (+ |hifrog::c::unsupported_op2varsignedbv!0#0| |func::1::m!0#16|)) (= |func::1::m!0#18| (+ |hifrog::c::unsupported_op2varsignedbv!0#0| |func::1::m!0#17|)) (= |func::1::m!0#19| (+ |hifrog::c::unsupported_op2varsignedbv!0#0| |func::1::m!0#18|)) (= |func::1::m!0#20| (+ |hifrog::c::unsupported_op2varsignedbv!0#0| |func::1::m!0#19|)) (= |func::1::m!0#21| (+ |hifrog::c::unsupported_op2varsignedbv!0#0| |func::1::m!0#20|)) (= |func::1::m!0#22| (+ |hifrog::c::unsupported_op2varsignedbv!0#0| |func::1::m!0#21|)) (= |func::1::m!0#23| (+ |hifrog::c::unsupported_op2varsignedbv!0#0| |func::1::m!0#22|)) (= |func::1::m!0#24| (+ |hifrog::c::unsupported_op2varsignedbv!0#0| |func::1::m!0#23|)) (= |func::1::m!0#25| (+ |hifrog::c::unsupported_op2varsignedbv!0#0| |func::1::m!0#24|)) (= |func::1::m!0#25| |func::$tmp::return_value!0#7|) (= |func::$tmp::return_value!0#8| .oite0) (= |func::$tmp::return_value!0#8| |func::#return_value!0#2|) (or |hifrog::fun_start!0#5| (not |hifrog::fun_end!0#5|)))
:named c))
; XXX Partition: 3
(assert (!
(and (= |func::a!0#3| |func::a!0#1|) (= |func::b!0#3| |func::b!0#1|) (= |goto_symex::guard#2| (>= (+ |func::a!0#3| |func::b!0#3|) 1)) (= |func::$tmp::return_value!0#1| (/ (+ |func::a!0#3| |func::b!0#3|) 2)) (= |hifrog::c::unsupported_op2varsignedbv!0#1| (uns_mod |func::a!0#3| |func::b!0#3|)) (= |func::1::m!0#3| (+ 1 |hifrog::c::unsupported_op2varsignedbv!0#1|)) (= |func::1::m!0#4| (+ |hifrog::c::unsupported_op2varsignedbv!0#1| |func::1::m!0#3|)) (= |func::1::m!0#5| (+ |hifrog::c::unsupported_op2varsignedbv!0#1| |func::1::m!0#4|)) (= |func::1::m!0#6| (+ |hifrog::c::unsupported_op2varsignedbv!0#1| |func::1::m!0#5|)) (= |func::1::m!0#7| (+ |hifrog::c::unsupported_op2varsignedbv!0#1| |func::1::m!0#6|)) (= |func::1::m!0#8| (+ |hifrog::c::unsupported_op2varsignedbv!0#1| |func::1::m!0#7|)) (= |func::1::m!0#9| (+ |hifrog::c::unsupported_op2varsignedbv!0#1| |func::1::m!0#8|)) (= |func::1::m!0#10| (+ |hifrog::c::unsupported_op2varsignedbv!0#1| |func::1::m!0#9|)) (= |func::1::m!0#11| (+ |hifrog::c::unsupported_op2varsignedbv!0#1| |func::1::m!0#10|)) (= |func::1::m!0#12| (+ |hifrog::c::unsupported_op2varsignedbv!0#1| |func::1::m!0#11|)) (= |func::1::m!0#12| |func::$tmp::return_value!0#3|) (= |func::$tmp::return_value!0#4| .oite1) (= |func::$tmp::return_value!0#4| |func::#return_value!0#1|) (or |hifrog::fun_start!0#4| (not |hifrog::fun_end!0#4|)))
:named d))
; XXX Partition: 2
(assert (!
(and (= |main::1::a!0#2| |symex::nondet#0|) (= |main::1::b!0#2| |symex::nondet#1|) (= |main::1::a!0#2| |main::1::c!0#2|) (= |main::1::b!0#2| |main::1::d!0#2|) (= |func::a!0#1| |main::1::a!0#2|) (= |func::b!0#1| |main::1::b!0#2|) (= |func::#return_value!0#1| |main::1::p!0#2|) (= |func::a!0#2| |main::1::c!0#2|) (= |func::b!0#2| |main::1::d!0#2|) (= |func::#return_value!0#2| |main::1::q!0#2|) (= (and (and (>= |main::1::b!0#2| -999) (not (>= |main::1::b!0#2| 1000))) (and |hifrog::fun_start!0#3| (and (>= |main::1::a!0#2| -999) (not (>= |main::1::a!0#2| 1000))))) |hifrog::fun_start!0#4|) (= (and |hifrog::fun_end!0#4| (and (and (>= |main::1::b!0#2| -999) (not (>= |main::1::b!0#2| 1000))) (and |hifrog::fun_start!0#3| (and (>= |main::1::a!0#2| -999) (not (>= |main::1::a!0#2| 1000)))))) |hifrog::fun_start!0#5|) (= (not (or (not (and |hifrog::fun_end!0#5| (and |hifrog::fun_end!0#4| (and (and (>= |main::1::b!0#2| -999) (not (>= |main::1::b!0#2| 1000))) (and |hifrog::fun_start!0#3| (and (>= |main::1::a!0#2| -999) (not (>= |main::1::a!0#2| 1000)))))))) (= |main::1::p!0#2| |main::1::q!0#2|))) |hifrog::?err!0#2|) (or (not |hifrog::fun_end!0#3|) (and |hifrog::fun_end!0#5| (and |hifrog::fun_end!0#4| (and (and (>= |main::1::b!0#2| -999) (not (>= |main::1::b!0#2| 1000))) (and |hifrog::fun_start!0#3| (and (>= |main::1::a!0#2| -999) (not (>= |main::1::a!0#2| 1000)))))))))
:named e))
; XXX Partition: 1
(assert (!
(or |hifrog::fun_start!0#2| (not |hifrog::fun_end!0#2|))
:named f))
; XXX Partition: 0
(assert (!
(and |hifrog::?err!0#2| |hifrog::fun_start!0#2| (= |hifrog::fun_end!0#2| |hifrog::fun_start!0#3|) (= |return'!0#1| |symex::io::0|))
:named g))
(check-sat)
(get-interpolants d (and a b c e f g))
